Nuprl Lemma : kindcase_wf
11,40
postcript
pdf
B
:Type,
k
:Knd,
f
:(Id
B
),
g
:(IdLnk
Id
B
). kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
,
t
))
B
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
;
t
))
,
x
(
s
)
,
x
(
s1
,
s2
)
,
if
b
then
t
else
f
fi
,
islocal(
k
)
,
act(
k
)
,
lnk(
k
)
,
tag(
k
)
,
b
,
isl(
x
)
,
outr(
x
)
,
t
.1
,
outl(
x
)
,
t
.2
,
tt
,
ff
,
Knd
Lemmas
IdLnk
wf
,
Id
wf
,
Knd
wf
origin
B:Type, k:Knd, f:(Id
B), g:(IdLnkIdB). kindcase(k; a.f(a); l,t.g(l,t)) 
B B:Type, k:Knd, f:(IdB), g:(IdLnkIdB). kindcase(k; a.f(a); l,t.g(l,t)) B x:A. B(x) T
b